Add progressive depth-halving policy to Prover.advance_proof#4925
Closed
Stevengre wants to merge 1 commit into
Closed
Add progressive depth-halving policy to Prover.advance_proof#4925Stevengre wants to merge 1 commit into
Stevengre wants to merge 1 commit into
Conversation
Implements runtimeverification#4924: factor kontrol's `--per-depth-timeout` mechanism out of tool-specific code and into a generic policy in `Prover.advance_proof`. When `per_depth_timeout` is set, each step gets a stall window of `current_depth * per_depth_timeout` seconds to commit. A step that exceeds its window is interrupted, the step depth is halved (floor 1), and the node is retried at the shallower depth; at the minimum depth the proof stops and stays pending. Provers that do not expose a tunable depth are unaffected, and the path without `per_depth_timeout` is unchanged. - Prover: generic no-op hooks get_step_depth/set_step_depth/interrupt - APRProver: overrides them (execute_depth + kcfg_explore.interrupt) - KCFGExplore/CTermSymbolic/KoreClient/JsonRpc*/Transport: interrupt() that force-unblocks an in-flight single-socket request and reconnects - Unit tests covering halving, stop-at-floor, fast-path, and disabled
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #4924.
Factors kontrol's
--per-depth-timeoutmechanism out of tool-specific code and into a generic policy inProver.advance_proof, as suggested by @ehildenb in this review comment.What it does
advance_proofgains an optionalper_depth_timeout: float | None = None. When set to a positive value (and the prover exposes a tunable step depth), eachstep_proofruns under a stall window ofcurrent_depth * per_depth_timeoutseconds:This mirrors the kontrol behavior (
--max-depth 1000 --per-depth-timeout 0.5→ 500s window, then 250s at depth 500, … down to depth 1) but as a reusable, in-process policy rather than a forked-subprocess kill loop.How it stays generic
The policy lives entirely in the base
Proverand is driven by three new hooks with safe no-op defaults:get_step_depth() -> int | None— returnNone(default) to opt out of the policy entirely.set_step_depth(depth)— no-op default.interrupt()— abort an in-flightstep_proofon another thread; no-op default.APRProveroverrides them to read/writeexecute_depthand to callkcfg_explore.interrupt(). Provers without a tunable depth are unaffected, and the code path whenper_depth_timeoutis unset is unchanged.To actually abort an in-flight Kore RPC call,
interrupt()is threaded throughKCFGExplore→CTermSymbolic→KoreClient→JsonRpcClientFacade/JsonRpcClient→Transport.SingleSocketTransport.interrupt()shuts down the blocked socket (unblocking the reader thread) and reconnects so the prover stays usable;HttpTransport.interrupt()is a documented no-op.Testing
pyk/src/tests/unit/test_advance_proof.py(in-memory fake prover, no backend): covers halving-until-progress, stop-at-minimum-depth, no-halving-when-fast, and the disabled (noper_depth_timeout) path.make -C pyk checkpasses (flake8, mypy, autoflake, isort, pydocstyle, black).Notes / follow-up
Client-side
interrupt()reconnects to the sameKoreServer(preserving added modules), but an abandoned computation may keep running server-side until it notices the dropped connection — unlike kontrol's full process-group kill. The shallower retry still proceeds correctly; a fully faithful server-restart variant would require the prover to own the server handle and is left as a follow-up.CLI flag plumbing remains on the tool side (e.g. kontrol); this PR only provides the generic capability.